Nuprl Lemma : weak-antecedent-surjection_wf
11,40
postcript
pdf
es
:ES,
P
,
Q
:(E
),
f
:({
e
:E|
P
(
e
)}
E).
Q
=
f
==
P
latex
Definitions
ES
,
t
T
,
Type
,
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
f
(
a
)
,
{
x
:
A
|
B
(
x
)}
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Q
==
f
==
P
,
P
&
Q
,
Q
=
f
==
P
Lemmas
weak-antecedent-function
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, P, Q:(E
), f:({e:E| P(e)} E). Q 
= f== P 
es:ES, P, Q:(E), f:({e:E| P(e)} E). Q = f== P Tx:A. B(x)B(x)
B(x)
x:A. B(x)==f== P= f== P